@ @p
bool:=#:atom. {blah}
proof(b:bool):=#:atom.

eq(a:atom;x,y:a):=#:bool.
is(a:atom;x,y:a):=proof(eq(a,x,y)):atom.
identical(a:atom;x:a):=#:is(a,x,x).
eq_axiom(a:atom;x,y,z:a;p:is(a,x,z);q:is(a,y,z)):=#:is(a,x,y).
eq_symmetry(a:atom;x,y:a;p:is(a,x,y)):=
 eq_axiom(a,y,x,y,identical(a,y),p):is(a,y,x).
eq_transitivity(a:atom;x,y,z:a;p:is(a,x,y);q:is(a,y,z)):=
 eq_axiom(a,x,z,y,p,eq_symmetry(a,y,z,q)):is(a,x,z).
eq_functionality(a,b:atom;x,y:a;p:is(a,x,y);f:(x:a)b):=#:is(b,f(x),f(y)).
@ @p

nat:=#:atom.
0:=#:nat.
succ(x:nat):=#:nat.
nat_pred(x:nat):=bool:atom.
nat_imp(p:nat_pred;x:nat;q:proof(p(x))):=proof(p(succ(x))):atom.
induction(p:nat_pred;q:proof(p(0));r:nat_imp(p)):=#:(x:nat)proof(p(x)).

is(x,y:nat):=is(nat,x,y):atom. {henceforth we'll talk only of |nat|s}

sum(x,y:nat):=#:nat.
sum_ax1(x:nat):=#:is(sum(x,0),x).
sum_ax2(x,y:nat):=#:is(sum(x,succ(y)),succ(sum(x,y))).

@ @p
thm1(x,y:nat):=eq(nat,sum(succ(x),y),succ(sum(x,y))):bool.
step1(x:nat):=sum_ax1(succ(x)):is(sum(succ(x),0),succ(x)).
step2(x:nat):=eq_functionality(nat,nat,sum(x,0),x,sum_ax1(x),succ):
 is(succ(sum(x,0)),succ(x)).
step3(x:nat):=
 eq_axiom(nat,sum(succ(x),0),succ(sum(x,0)),succ(x),step1(x),step2(x)):
 proof(thm1(x,0)).
step4(x,y:nat;q:proof(thm1(x,y))):=
 eq_axiom(nat,sum(succ(x),y),sum(x,succ(y)),succ(sum(x,y)),q,sum_ax2(x,y)):
 is(sum(succ(x),y),sum(x,succ(y))).
@ @p
step5(x,y:nat;q:proof(thm1(x,y))):=
 eq_functionality(nat,nat,sum(succ(x),y),sum(x,succ(y)),step4(x,y,q),succ):
 is(succ(sum(succ(x),y)),succ(sum(x,succ(y)))).
step6(x,y:nat):=sum_ax2(succ(x),y):
 is(sum(succ(x),succ(y)),succ(sum(succ(x),y))).
step7(x,y:nat;q:proof(thm1(x,y))):=
 eq_transitivity(nat,sum(succ(x),succ(y)),succ(sum(succ(x),y)),
  succ(sum(x,succ(y))),step6(x,y),step5(x,y,q)):
 proof(thm1(x,succ(y))).
qed_thm1(x:nat):=induction(thm1(x),step3(x),step7(x)):
 (y:nat)proof(thm1(x,y)).

thm2(x,y:nat):=eq(nat,sum(x,y),sum(y,x)):bool.